ForMath: Formalisation of Mathematics
| ForMath is an EU FP7 STREP FET-open project lead by Thierry Coquand at University of Gothenburg. March 2010--July 2013, Grant agreement nr. 243847 For any matter related to the project please contact the project manager Ana Bove. (Glossary: FP7 = Seventh Framework Programme; STREP = Specific Targeted Research Projects; FET = Future and Emerging Technologies) |  |  |
The project has now ended. The experts appointed by the European Commission judged this project achieved excellent results.
Table of contents:
Project Summary
Mathematics is already playing a crucial role in the design of sophisticated systems that are used daily as for example in geometrical modelling, robotics, cryptography, ... This use of mathematics will only increase, and issues of correctness and reliable specification of these systems will become more and more important. Besides its purely conceptual interest, the development of formalised mathematics is a promising way to tackle new technological challenges.
Concretely, the objective of this project is to develop libraries of formalised mathematics concerning algebra, linear algebra, real number computation, and algebraic topology. The libraries that we plan to develop in this proposal are especially chosen to have long-term applications in areas where software interacts with the physical world. The main originality of the work is to structure these libraries as a software development, relying on a basis that has already shown its power in the formal proof of the four-colour theorem, and to address topics that were mostly left untouched by previous research in formal proof or formal methods.
The main milestones of this work will concern formally proved algorithms for solving problems in real arithmetics and in algebraic topology. We have entered an era of mathematical proofs of extraordinary complexity that may indicate a change in our understanding of mathematical reasoning. Two examples of such complex proofs are the four-colour theorem, and
the recent solution by T. Hales of the Kepler conjecture, that both involve computers in a crucial way. Can we trust
such proofs? To address this problem, mathematicians and computer scientists have started research on formal proofs,
where every logical inference step can be checked by a computer. With interactive computer-based proof systems,
researchers can verify algorithms whenever a complete mathematical specification is feasible. So practically, the goal of this project is to make formal proof verification available to domains that were hitherto beyond the reach of proof systems.
List of Beneficiaries
- University of Gothenburg (UGOT): Thierry Coquand, Anders Mörtberg, Vincent Siles.
Project manager Ana Bove. - Radboud University Nijmegen (SKU): Bas Spitters, Herman Geuvers, Jelle Herold, Robbert Krebbers, Evgeny Makarov, Egbert Rijke, Eelis van der Weegen.
- INRIA: Yves Bertot, Cyril Cohen, Maxime Denčs, Georges Gonthier (Microsoft Research),Victor Magron, Assia Mahboubi, Loďc Pottier, Laurence Rideau, Enrico Tassi, Laurent Théry, Benjamin Werner.
- Universidad de La Rioja (ULR): Julio Rubio, Laureano Lambán, César Domínguez, Jesús Aransay, Vico Pascual, Jónathan Heras, María Poza, Jose Divasón, Rubén Sáenz.